Incremental Proof of the Producer/Consumer Property for the PCI Protocol
Identifieur interne : 008794 ( Main/Exploration ); précédent : 008793; suivant : 008795Incremental Proof of the Producer/Consumer Property for the PCI Protocol
Auteurs : Dominique Cansell [France] ; Ganesh Gopalakrishnan [États-Unis] ; Mike Jones [États-Unis] ; Dominique Méry [France] ; Airy Weinzoepflen [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
Abstract: We present an incremental proof of the producer/consumer property for the PCI protocol. In the incremental proof, a corrected model of the multi-bus PCI 2.1 protocol is shown to be a refinement of the producer/consumer property. Multi-bus PCI must be corrected because the original PCI specification violates the producer/consumer property. The final model of PCI includes transaction types and reordering along with the completion mechanism for delayed PCI transactions. Verification results include multiple concurrent sessions of the producer/consumer property in a family of topologically isomorphic network configurations. The remaining configurations are identified and left for future work. In contrast to previous case studies involving this problem [13],[15], the incremental proof provides structure which simplifies otherwise difficult monolithic proof attempts.
Url:
DOI: 10.1007/3-540-45648-1_2
Affiliations:
- France, États-Unis
- Grand Est, Lorraine (région), Utah
- Nancy
- Centre national de la recherche scientifique, Institut national de recherche en informatique et en automatique, Laboratoire lorrain de recherche en informatique et ses applications, Mosel (Loria), Université de Lorraine
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003726
- to stream Istex, to step Curation: 003683
- to stream Istex, to step Checkpoint: 001C30
- to stream Main, to step Merge: 008C50
- to stream PascalFrancis, to step Corpus: 000881
- to stream PascalFrancis, to step Curation: 000171
- to stream PascalFrancis, to step Checkpoint: 000801
- to stream Main, to step Merge: 008D86
- to stream Main, to step Curation: 008794
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Incremental Proof of the Producer/Consumer Property for the PCI Protocol</title><author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name><affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="region" nuts="2">Lorraine (région)</region></placeName><orgName type="team" n="7">Mosel (Loria)</orgName><orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName><orgName type="university">Université de Lorraine</orgName><orgName type="EPST">Centre national de la recherche scientifique</orgName><orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName></affiliation></author><author><name sortKey="Gopalakrishnan, Ganesh" sort="Gopalakrishnan, Ganesh" uniqKey="Gopalakrishnan G" first="Ganesh" last="Gopalakrishnan">Ganesh Gopalakrishnan</name></author><author><name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name></author><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="region" nuts="2">Lorraine (région)</region></placeName><orgName type="team" n="7">Mosel (Loria)</orgName><orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName><orgName type="university">Université de Lorraine</orgName><orgName type="EPST">Centre national de la recherche scientifique</orgName><orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName></affiliation></author><author><name sortKey="Weinzoepflen, Airy" sort="Weinzoepflen, Airy" uniqKey="Weinzoepflen A" first="Airy" last="Weinzoepflen">Airy Weinzoepflen</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:E621210A3538DB1E250A1A09F796F0A4511A6421</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1007/3-540-45648-1_2</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-VVP7FG8X-1/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003726</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003726</idno><idno type="wicri:Area/Istex/Curation">003683</idno><idno type="wicri:Area/Istex/Checkpoint">001C30</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001C30</idno><idno type="wicri:doubleKey">0302-9743:2002:Cansell D:incremental:proof:of</idno><idno type="wicri:Area/Main/Merge">008C50</idno><idno type="wicri:source">INIST</idno><idno type="RBID">Pascal:02-0202115</idno><idno type="wicri:Area/PascalFrancis/Corpus">000881</idno><idno type="wicri:Area/PascalFrancis/Curation">000171</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000801</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000801</idno><idno type="wicri:doubleKey">0302-9743:2002:Cansell D:incremental:proof:of</idno><idno type="wicri:Area/Main/Merge">008D86</idno><idno type="wicri:Area/Main/Curation">008794</idno><idno type="wicri:Area/Main/Exploration">008794</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Incremental Proof of the Producer/Consumer Property for the PCI Protocol</title><author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LORIA, Nancy</wicri:regionArea><placeName><region type="region">Grand Est</region><region type="old region">Lorraine (région)</region><settlement type="city">Nancy</settlement></placeName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="region" nuts="2">Lorraine (région)</region></placeName><orgName type="team" n="7">Mosel (Loria)</orgName><orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName><orgName type="university">Université de Lorraine</orgName><orgName type="EPST">Centre national de la recherche scientifique</orgName><orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="region" nuts="2">Lorraine (région)</region></placeName><orgName type="team" n="7">Mosel (Loria)</orgName><orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName><orgName type="university">Université de Lorraine</orgName><orgName type="EPST">Centre national de la recherche scientifique</orgName><orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName></affiliation></author><author><name sortKey="Gopalakrishnan, Ganesh" sort="Gopalakrishnan, Ganesh" uniqKey="Gopalakrishnan G" first="Ganesh" last="Gopalakrishnan">Ganesh Gopalakrishnan</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><wicri:regionArea>University of Utah, Salt Lake City, Utah</wicri:regionArea><placeName><region type="state">Utah</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">États-Unis</country></affiliation></author><author><name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><wicri:regionArea>presently at Brigham Young University, Provo, Utah</wicri:regionArea><placeName><region type="state">Utah</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">États-Unis</country></affiliation></author><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LORIA, Nancy</wicri:regionArea><placeName><region type="region">Grand Est</region><region type="old region">Lorraine (région)</region><settlement type="city">Nancy</settlement></placeName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="region" nuts="2">Lorraine (région)</region></placeName><orgName type="team" n="7">Mosel (Loria)</orgName><orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName><orgName type="university">Université de Lorraine</orgName><orgName type="EPST">Centre national de la recherche scientifique</orgName><orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="region" nuts="2">Lorraine (région)</region></placeName><orgName type="team" n="7">Mosel (Loria)</orgName><orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName><orgName type="university">Université de Lorraine</orgName><orgName type="EPST">Centre national de la recherche scientifique</orgName><orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName></affiliation></author><author><name sortKey="Weinzoepflen, Airy" sort="Weinzoepflen, Airy" uniqKey="Weinzoepflen A" first="Airy" last="Weinzoepflen">Airy Weinzoepflen</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LORIA, Nancy</wicri:regionArea><placeName><region type="region">Grand Est</region><region type="old region">Lorraine (région)</region><settlement type="city">Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Formal specification</term><term>Program verification</term><term>Refinement method</term><term>Theorem proving</term><term>Transmission protocol</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Démonstration théorème</term><term>Méthode raffinement</term><term>Protocole transmission</term><term>Spécification formelle</term><term>Vérification programme</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We present an incremental proof of the producer/consumer property for the PCI protocol. In the incremental proof, a corrected model of the multi-bus PCI 2.1 protocol is shown to be a refinement of the producer/consumer property. Multi-bus PCI must be corrected because the original PCI specification violates the producer/consumer property. The final model of PCI includes transaction types and reordering along with the completion mechanism for delayed PCI transactions. Verification results include multiple concurrent sessions of the producer/consumer property in a family of topologically isomorphic network configurations. The remaining configurations are identified and left for future work. In contrast to previous case studies involving this problem [13],[15], the incremental proof provides structure which simplifies otherwise difficult monolithic proof attempts.</div></front></TEI><affiliations><list><country><li>France</li><li>États-Unis</li></country><region><li>Grand Est</li><li>Lorraine (région)</li><li>Utah</li></region><settlement><li>Nancy</li></settlement><orgName><li>Centre national de la recherche scientifique</li><li>Institut national de recherche en informatique et en automatique</li><li>Laboratoire lorrain de recherche en informatique et ses applications</li><li>Mosel (Loria)</li><li>Université de Lorraine</li></orgName></list><tree><country name="France"><region name="Grand Est"><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name></region><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><name sortKey="Weinzoepflen, Airy" sort="Weinzoepflen, Airy" uniqKey="Weinzoepflen A" first="Airy" last="Weinzoepflen">Airy Weinzoepflen</name><name sortKey="Weinzoepflen, Airy" sort="Weinzoepflen, Airy" uniqKey="Weinzoepflen A" first="Airy" last="Weinzoepflen">Airy Weinzoepflen</name></country><country name="États-Unis"><region name="Utah"><name sortKey="Gopalakrishnan, Ganesh" sort="Gopalakrishnan, Ganesh" uniqKey="Gopalakrishnan G" first="Ganesh" last="Gopalakrishnan">Ganesh Gopalakrishnan</name></region><name sortKey="Gopalakrishnan, Ganesh" sort="Gopalakrishnan, Ganesh" uniqKey="Gopalakrishnan G" first="Ganesh" last="Gopalakrishnan">Ganesh Gopalakrishnan</name><name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name><name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 008794 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 008794 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:E621210A3538DB1E250A1A09F796F0A4511A6421
|texte= Incremental Proof of the Producer/Consumer Property for the PCI Protocol
}}
| This area was generated with Dilib version V0.6.33. |  |